A, B:Type, g:(A(B + Top)), X:MaInterface(A). ma-interface-compose(g;X)  MaInterface(B) 

latex

Definitions	Type, t  T, Top, left + right, x:AB(x), {x:A| B(x)} , Knd, b, x:A. B(x), State(ds), x:A  B(x), hasloc(k;i), x. t(x), a:A fp B(a), Id, (x  l), type List, f(a), f o g  , x.A(x), <a, b>, let x,y = A in B(x;y), x:A.B(x), g o f, ma-interface-compose(g;X), MaInterface(T)
Lemmas	fpf-compose wf, p-compose wf, l member wf, Id wf, fpf wf, Knd wf, assert wf, hasloc wf, decl-state wf, top wf